$\forall$$w$:World, $e$:E. $\neg$first($e$) $\Rightarrow$ ($\forall$$t$:$\mathbb{N}$. time(pred($e$))+1$\leq$$t$ $\Rightarrow$ $t$$<$time($e$) $\Rightarrow$ isnull(a(loc($e$);$t$)))